Termination Proof Script
Consider the TRS R consisting of the rewrite rules
1:
0
-
y
→
0
2:
x
-
0
→ x
3:
x
-
s
(y)
→
if
(
greater
(x,
s
(y)),
s
(x
-
p
(
s
(y))),
0
)
4:
p
(
0
)
→
0
5:
p
(
s
(x))
→ x
There are 2 dependency pairs:
6:
x
-#
s
(y)
→ x
-#
p
(
s
(y))
7:
x
-#
s
(y)
→
P
(
s
(y))
The approximated dependency graph contains one SCC: {6}.
Consider the SCC {6}. The usable rules are {4,5}.
The constraints could not be solved.
Tyrolean Termination Tool
(0.01 seconds) --- May 3, 2006